Nuprl Lemma : es-interval-non-zero
0,22
postcript
pdf
es
:ES,
e
,
e'
:E.
e
e'
0<||[
e
,
e'
]||
latex
Definitions
ES
,
t
T
,
x
:
A
.
B
(
x
)
,
E
,
[
e
,
e'
]
,
||
as
||
,
Prop
,
e
e'
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
i
j
,
False
,
A
,
A
B
,
(
x
l
)
,
x
:
A
.
B
(
x
)
,
Trans
x
,
y
:
T
.
E
(
x
;
y
)
Lemmas
es-le-trans
,
not
functionality
wrt
iff
,
length
zero
,
member
exists
,
nil
member
,
l
member
wf
,
member-es-interval
,
es-le-self
,
pos
length
,
es-le
wf
,
length
wf1
,
es-interval
wf
,
es-E
wf
,
event
system
wf
origin
es:ES, e, e':E. e 
e' 
0<||[e, e']|| es:ES, e, e':E. e e' 0<||[e, e']|| 
Tx:A. B(x) e' 
Q Q Q
j
AB l)
x:A. B(x)